%\documentclass[orivec]{llncs}
 \documentclass[preprint,11pt]{elsarticle}
 
\usepackage{intestazione2}
%\usepackage{times}
\usepackage{macron}
\usepackage{geometry}
%\usepackage{bbold}


\begin{document}

%
%\frontmatter          
%\pagestyle{headings}  
%%
%\mainmatter           

\begin{frontmatter}
\title{Disciplined Structured Communications with \\ Disciplined Adaptation}
\author[evry]{Cinzia Di Giusto} 
\author[unl]{Jorge A. P\'{e}rez}

%\cortext[cor1]{Corresponding author}  
\address[evry]{Universit\'e d'Evry - Val d'Essonne, IBISC}
\address[unl]{CITI and Departamento de Inform\'atica, FCT Universidade Nova de Lisboa}


     
\begin{abstract}
\emph{Session types} offer a powerful
%have been intensively studied as 
%formal models 
 type-the\-o\-ret\-ic foundation for the analysis of 
%complex scenarios of 
structured communications, as commonly found in serv\-ice-oriented systems.
They are defined upon core programming calculi which offer only limited support 
%lack explicit constructs 
for expressing adaptation and evolvability requirements.
This is unfortunate, as serv\-ice\--ori\-ented systems are increasingly being deployed upon %open, 
highly dynamic infrastructures in which such requirements are 
%fundamental 
central concerns.
%central in ensuring reliable system operation. % and business agility.
In previous work, we developed a process calculi framework of \emph{adaptable processes},
in which concurrent processes can be replaced,  suspended, or discarded at runtime.
%as an attempt to enhance process calculi specifications with evolvability concerns.
In this paper, we %extend %integrate adaptable processes into 
propose a session types discipline for a calculus with adaptable processes. 
%The resulting 
Our framework offers an alternative for integrating runtime adaptation mechanisms  in 
the analysis of structured communications.
We show that well-typed processes enjoy \emph{consistency}:
communicating behavior is never interrupted by evolvability actions. 
\end{abstract}

\end{frontmatter}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\section{Introduction}

\emph{Session types} 
%have been intensively studied as 
offer a powerful type-theoretic foundation 
%formal models 
for the analysis of
%represent one of the most studied foundations for analyzing 
complex scenarios of structured communications, as frequently found in service-oriented systems.  
They abstract communication protocols as basic interaction patterns, which
%. As a simple example, 
%the session type
%$?(\mathsf{tweet}).!(\mathsf{ok}). \epsilon$
%can be assigned to a server that first \emph{receives} a value of type $\mathsf{tweet}$, then \emph{sends} a value of type $\mathsf{ok}$, 
%and \emph{finishes}. 
%These basic patterns
are then statically checked against specifications
in some core programming calculus---typ\-i\-cal\-ly, a variant of the $\pi$-calculus.
%This way, e.g., the session type
%$?(\mathsf{tweet}).!(\mathsf{ok}). \epsilon$
%can be assigned to a server that first \emph{receives} a value of type $\mathsf{tweet}$, then \emph{sends} a value of type $\mathsf{ok}$, 
%and \emph{finishes}. 
%Correctness is enforced through \emph{duality}: 
%our server will interact correctly only with clients with type $!(\mathsf{tweet}).?(\mathsf{ok}). \epsilon$.
Introduced in~\cite{DBLP:conf/concur/Honda93,DBLP:conf/esop/HondaVK98}, 
session type theories 
have been extended in many directions---see~\cite{DBLP:conf/wsfm/Dezani-Ciancaglinid09} for a survey.
%so as to cover, e.g., %forms of 
%higher-order~\cite{DBLP:conf/tlca/MostrousY07} and 
%multiparty~\cite{DBLP:conf/popl/HondaYC08} %, and asynchronous~\cite{DBLP:conf/forte/KouzapasYH11} 
%communication. % (See~\cite{DBLP:conf/wsfm/Dezani-Ciancaglinid09} for a survey.)
Their practical relevance %of session types 
is witnessed by, e.g., 
%functional~\cite{DBLP:conf/haskell/PucellaT08} and object-oriented~\cite{DBLP:conf/coordination/NgYPHK11} implementations, and by 
 their application in the verification of parallel systems~\cite{DBLP:conf/tools/NgYH12}.


%However, and in 
In spite of these developments, 
we find that existing ses\-sion-typed
%programming 
calculi do not explicitly support 
for reasoning about \emph{runtime adaptation}. % such as runtime adaptation and dynamic reconfiguration.
%}\footnote{Name passing can be considered a form of dynamic reconfiguration}
While channel mobility (\emph{delegation}~\cite{DBLP:journals/entcs/YoshidaV07}) 
as supported by such calculi
is often useful to model forms of
dynamic reconfiguration, more general forms of adaptation/evolvability 
are not expressible or are hard to reason about.
%Adaptation and evolvability are increasingly relevant issues nowadays, 
Runtime adaptation is an increasingly relevant issue nowadays, 
as distributed systems and applications are  being deployed in
open, highly dynamic infrastructures, such as cloud computing platforms.
In such settings,  
runtime adaptation %and dynamic reconfiguration  
appears as a key feature to
%are central capabilities to 
ensure continued system operation,
reduce costs, and achieve
business agility. %\todo{maybe a sentence on sessions here}

We thus observe a rather unfortunate discrepancy between 
(i)~the evolvability capabilities of modern distributed systems in practice, and 
(ii)~the forms of interaction available in the calculi 
upon which session types disciplines are defined.
 %(essentially, variants of the $\pi$-calculus)


In this paper, we propose an approach towards overcoming this discrepancy.
We %extend an existing 
introduce a
session types discipline 
for a language
equipped
with 
mechanisms for runtime adaptation.
Rather than developing yet another session types discipline \emph{from scratch}, we have deliberately 
preferred to build upon two existing lines of work. 
Our proposal %approach types discipline 
 results from combining 
the %main insights of the 
framework of 
\emph{adaptable processes}, which we have developed together with Bravetti and Zavattaro in~\cite{BGPZFMOODS}, with
the main insights %principles %underlying the discipline 
of the session type system
put forward by Garralda et al.~\cite{DBLP:conf/ppdp/GarraldaCD06}. 
%On the one hand, based on a limited form of higher-order communication, 
While %the framework in~\cite{BGPZFMOODS} 
adaptable processes
%While the latter work
represent an attempt for enhancing process calculi specifications with evolvability mechanisms, 
%the former . On the other hand, 
the work in~\cite{DBLP:conf/ppdp/GarraldaCD06} 
develops a %theory for \emph{safe}\footnote{\small{In~\cite{DBLP:conf/ppdp/GarraldaCD06}, \emph{safety} refers to the proper interaction of mobility steps and communication, and so it differs from the usual notion of type safety. To avoid confusion, here we use the adjective \emph{consistent}.}} 
session types theory for the Boxed Ambient calculus~\cite{DBLP:journals/toplas/BugliesiCC04}.
Despite these seemingly distant origins, %we believe that 
our framework %presented here %, we believe,
combines the most interesting ideas of both approaches into a simple yet expressive model 
of structured communications with explicit mechanisms for runtime adaptation.

We briefly describe our approach and results. 
%We consider a
Our  process language includes
%equipped with 
a set of standard $\pi$-calculus constructs, extended 
with the \emph{located processes} and the \emph{update processes} introduced in~\cite{BGPZFMOODS}.
Given a location $l$, a process $P$, and a context $Q(\mathsf{X})$ 
(i.e. a process with free occurrences of variable $\mathsf{X}$), these processes are noted $l[P]$ and $l\{Q(\mathsf{X})\}$, resp. 
They may interact so as to evolve into process 
$Q\subst{P}{\mathsf{X}}$, which represents the \emph{update} of  process $P$ at $l$ with a reconfiguration routine 
(or built-in adaptation mechanism)
embodied by $Q(\mathsf{X})$. Locations can be nested and are transparent:
within $l[P]$, process $P$ can evolve autonomously, with the potential of interacting with some neighboring 
update process $l\{Q(\mathsf{X})\}$, as just described. 
Hence, %This way, 
%in the adaptable processes %intuitive description may be useful to realize how in the framework of~\cite{BGPZFMOODS} 
%framework evolvability corresponds to a form of (higher-order) process mobility. 
in our language communicating behavior coexists with update actions. 
This raises the need for disciplining both forms of interaction, 
respecting session types descriptions but also enforcing evolvability requirements. 
To this end, by observing that %exploiting the fact that 
update corresponds to a form of (higher-order) process mobility, 
%This observation is the key to understand the relationship 
%we establish a relationship with the session types 
we draw inspiration from the session types 
in~\cite{DBLP:conf/ppdp/GarraldaCD06}.
Indeed, 
%by injecting in the syntax some constructs supporting static analysis,
such a type discipline 
%a main contribution of
%in~\cite{DBLP:conf/ppdp/GarraldaCD06} %is the technical machinery that 
ensures that
session communications within Ambient hierarchies %are \emph{safe}, i.e., they 
do not get interrupted by Ambient mobility steps. 
We call this property \emph{session consistency}.

While both Ambients and adaptable processes rely on nested located processes,
Ambient mobility and evolvability steps are conceptually very different.
In fact, %is a major difference:
%The main difference between the two is that, while 
Ambient mobility is only defined in a parent-child style, whereas
%in~\cite{BGPZFMOODS}
%synchronizations between 
located processes and update actions 
 may interact independently of their relative position in the hierarchy induced by location nesting.
This way, integrating our calculus for adaptable processes %of~\cite{BGPZFMOODS} 
with the session types discipline in~\cite{DBLP:conf/ppdp/GarraldaCD06}
roughly amounts to: 
(1)~generalizing the operational semantics of~\cite{DBLP:conf/ppdp/GarraldaCD06}
so as to account for adaptation in \emph{arbitrary process hierarchies}; 
(2)~endowing the evolvability constructs %of~\cite{BGPZFMOODS} 
with suitable \emph{annotations}, describing the session behavior embodied in located and update processes; and 
(3)~extending the typing judgments of~\cite{DBLP:conf/ppdp/GarraldaCD06}, so as to be able to reason about 
\emph{process interfaces}.
%``offered behavior'', 
%as described by the annotations described in (2). 
Ultimately, this last step is what realizes a form of \emph{typeful adaptation}, which contrasts with the untyped adaptation in~\cite{BGPZFMOODS}.  Well-typed processes 
in our framework
satisfy basic correctness guarantees (formalized as a Subject Reduction result), 
which entails consistency for session-typed processes %that
%including the \emph{session safety} of~\cite{DBLP:conf/ppdp/GarraldaCD06} (here called \emph{consistency}), adapted to the case of processes which 
%may be updated at runtime.
with runtime adaptation mechanisms.

This work is an initial %yet concrete 
step towards a theory of interaction
in which processes---endowed with behavioral disciplines expressed as types---may dynamically evolve at runtime. 
We have focused on session consistency---a basic 
approach to discipline
%consequence of considering 
the interplay of evolvability steps 
%(represented by the update of located processes) 
and communication behavior. % (represented by session interactions).
Issues such as deadlock-freedom, resource usage, and trustworthiness %, and reliability 
are also important---we plan to look into these in the future. 
Nevertheless, we believe that a major contribution of our paper %is novel, as it 
is to address issues which, to our knowledge, have not yet  been explored in the realm of 
%formal models for the specification and verification of distributed systems, such.
session-typed %interacting 
processes. \\

\noindent\textbf{Organization.~}
%The rest of the paper is structured as follows:
Sect.~\ref{sec:syn} presents our process language, and Sect.~\ref{s:types} defines our session type system.
In Sect.~\ref{sec:res} we state our main results (subject reduction and session consistency); an illustrative example is given in Sect.~\ref{sec:exam}.
We discuss interface compatibility for update actions in Sect.\ref{sec:int}.
Finally, Sect.~\ref{sec:rw} discusses related work and Sect.~\ref{sec:conc} collects some concluding remarks.
%An extended version of this paper, with proofs and additional examples, is available online.\footnote{{\scriptsize \url{http://www.jorgeaperez.net/publications/sac13ext.pdf}}}
%and discussions is~\cite{dGP-long}.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\newpage
\section{The Process Language}\label{sec:syn}
%\todo{I would not call this the \evol{} calculus: I would do the other way around, namely saying this is a pi-calculus
%with adaptable processes}
%
%\todo{Saying that we are presenting the process language and then presenting the type system is very strange.
%I realize Dezani does like this, but it doesn't make sense for them either}

%\paragraph{Syntax} 
We extend standard session-typed languages~\cite{DBLP:conf/esop/HondaVK98}
with \emph{located processes} and \emph{update actions}.
These constructs allow us to explicitly represent adaptation mechanisms in models of structured communications.
As in~\cite{DBLP:conf/ppdp/GarraldaCD06}, 
our process language 
is instrumented with some elements which support the static analysis.
In particular, we %consider
%annotated versions of the constructs defined in~\cite{BGPZFMOODS};
%as we will see, such annotations are key in statically ensuring consistent session behavior. Also,  namely 
annotate 
located processes with an integer (representing established sessions) and 
update actions  with 
%\emph{session types}---denoted $\ST_\qua$\,---and 
\emph{interfaces} $\INT$--- collections of session types (cf. 
%Both elements are introduced in 
Def.~\ref{d:types}.)

Our syntax builds upon the following  
base sets: 
\emph{names}, ranged over $a, b, x, y, \ldots$;
\emph{(polarized) channels}, ranged over $\cha^{+}, \cha^{-}, \ldots$;
\emph{locations}, ranged over $l, l', \ldots$;
\emph{labels}, ranged over $n, n', \ldots$;
\emph{process variables}, ranged over $\mathsf{X}, \mathsf{X}', \ldots$;
\emph{constants} (integers, booleans, names), ranged over $c, c', \ldots$;
\emph{recursion variables}, ranged over $Y, Y', \ldots$;
and \emph{integers}, ranged over $j,h,\ldots$.
While identifier $k$ stands for channels $\cha$ and names $x$, we use $u, u', \ldots$ to denote names and channels.
Then, \emph{processes}, ranged over $P, Q, R, \ldots$
and \emph{expressions}, ranged over $e, e', \ldots$
are given by the grammar in Table \ref{tab:syntax}.
%\todo{the idea is to send expressions, rather than values, assuming that $e \downarrow k$, i.e, 
%that expressions evaluate to constants. Still to add: expressions in the syntax, polyadicity.
%This is following~\cite{DBLP:conf/esop/HondaVK98}}
%We now give the syntax of processes. Some of the constructs are annotated with typing information; this is useful to ensure properties by static analysis.

%We propose here a variant of the \evol{} calculus \cite{BGPZFMOODS} that on top of the constructs that handle dynamic updates adds operators and annotations that are meant to implement safe sessions. 
%More precisely, the \evol{} language is based on the classical CCS constructs: input/output operators, parallel composition, recursion. To this first set of basic operators we add the ability of modeling systems that can dynamically update: thus adding locations and a special operator to update the content of locations. Finally we add a group of operators that implement sessions. 





%\begin{definition}[Syntax]\label{d:syntax}
%Processes are defined by the grammar in Table \ref{tab:syntax}.
%\begin{table*}[ht]
%$$
%\begin{array}{lclr}
%P & ::=  
%  	& c(x{:}\capab).P \sepr \outC{c}{v}.P & \text{Input/Output}\\
%  	& \sepr & \ifte{x=v}{P}{P} & \text{Conditional}\\
%  	& \sepr & P \para  P \sepr \rec{X{:}\type{\Phi}{\Delta}}{P_X}& \text{Parallel, Recursion}\\	 
%	&\sepr& \component{l}{h}{\Delta}{P} ~~(h \geq 0) ~\sepr \updated{l}{X}{\Delta}{\Delta'}{U} & \text{Adaptable Process, Update Process}\\
%	&\sepr& \open{c:\rho}.P \sepr \close{c}.P & \text{Open/Close Session}	\\
%	&\sepr& \branch{c}{n:P \dots n:P} \sepr \select{c}{n}.P ~~~& \text{Branch and Select}\\
%	&\sepr& \restr{c}{P}  & \text{Channel hiding}	\\
%U	&::= & P_{\mathsf{X}} &\text{Update}
%\end{array}
%$$
%\caption{Syntax of processes.} \label{tab:syntax}
%\end{table*}
\begin{table}[t]
$$
\begin{array}{lrlr}
P & ::=  &   \nopenr{a}{x}.P  & \text{session request}	\\
	& \sepr &   \nopena{a}{x}.P  & \text{session acceptance}	\\
	& \sepr &  \outC{k}{\tilde{e}}.P & \text{data output}\\
  	&\sepr &    \inC{k}{\tilde{x}}.P  & \text{data input}\\
	& \sepr &  \throw{k}{d}.P & \text{channel output}\\
    &\sepr &   \catch{k}{x}.P  & \text{channel input}\\
    	&\sepr&   \branch{k}{n_i:P_i}_{i \in I} & \text{branching}\\
	&\sepr&   \select{k}{n}.P & \text{selection}\\
	&\sepr&  \component{l}{h}{\Delta}{P} ~~(h \geq 0)  & \text{adaptable process}\\
    & \sepr &   \mathsf{X}& \text{process variable} \\
	&\sepr&  \updated{l}{X}{\INT_1}{\INT_2}{P} & \text{update process}\\
  	& \sepr &  \ifte{e}{P}{Q} & \text{conditional}\\
  	& \sepr &   P \para  P & \text{parallel composition}\\	 
		&\sepr&   \close{k}.P & \text{close session}	\\
			&\sepr&   \restr{u}{P}  & \text{name/channel hiding}	\\
				    & \sepr &   Y& \text{recursion variable}\\	 
	& \sepr &   \rec{Y{:}\ActS{\cdot}\INT}{P}& \text{recursion}\\	
			&\sepr&   \mathbf{0}  & \text{inaction} \\
%p	&::= &  + \sepr - &\text{channel polarities} \\
e	&::= &  c &\text{constants} \\
    & \sepr &   e_1 + e_2 \sepr e_1 - e_2  \sepr \ldots & \text{operators}
\end{array} 
$$
%\vspace{-4mm}
\caption{Process Syntax} \label{tab:syntax}
\end{table}
%\end{definition}

%\todo{Look for a nice and concise definition of U}

%Some comments to the processes in Table~\ref{tab:syntax} are in order. % for denoting the hole in a context $P(\mathsf{X})$. 
%The former are  whereas the latter are written ; 
%for simplicity, we write $\mathcal{X}, \mathcal{X}', \ldots$ to refer to either kind.

%We write $P_{\mathsf{X}}$ to refer to processes with occurrences of variables, in such a way
%that each $\mathsf{X}$ is bound to a context $U$. 
%(Analogously for recursion variables, for which we write $P_X$.)
%Also, we assume that names $l, l', \ldots$---used to denote process locations---come from a set that is disjoint from the set containing 
%$c, c', \ldots$, which are typically used to denote 
%communication channels.


%\begin{table}[t]
%$$
%\begin{array}{ll}
%(P \para  Q) \para  R \equiv P \para  (Q \para  R)\\
%
%P \para  Q \equiv Q \para  P & P \para  \nil \equiv P \\
%
%\restr{a}{P} \para  Q \equiv \restr{a}{P \para  Q}&
%\restr{a}{\nil} \equiv \nil\\
%\restr{a}{\restr{b}{P}} \equiv \restr{b}{\restr{a}{P}} & 
%\restr{a}{\component{l}{h}{\Delta}{P}} \equiv \component{l}{h}{\Delta}{\restr{a}{P}}
%\end{array}
%$$
%\caption{Structural congruence rules} \label{tab:congruence}
%\end{table}







We comment on the non-standard constructs in Table~\ref{tab:syntax}; 
intuitions and conventions for the other constructs are as in~\cite{DBLP:conf/esop/HondaVK98}.
Prefixes $\nopena{a}{x}$  and $\nopenr{a}{y}$ use name $a$ to establish a new session;
process 
$\close{k}.P$ 
is used to explicitly terminate a session on $k$.
Once established, structured behavior on channels is possible.
The exchange of expressions 
(with the expected simultaneous substitution $\sub{\tilde{k}}{\tilde{x}}$)
is as usual; channel passing  
(delegation) is also supported.
Thus, our language features the usual dynamic reconfiguration via channel passing
as well as runtime adaptation via \emph{located} and \emph{update processes}, as we explain next.

%$\component{l}{h}{\Delta}{Q}$
A \emph{located process} $\component{l}{h}{\Delta}{Q}$ denotes a
process $Q$  deployed at location $l$.
Inside $l$, process $Q$ can evolve on its own and interact with external processes;
we use $l$ as a reference for a potential update actions (see below).
In $\component{l}{h}{\Delta}{Q}$, 
%while $\Delta$ describes the interface of $Q$, 
$h$ stands for the number of active sessions in $Q$: 
our operational semantics uses this information to ensure that locations enclosing active 
sessions are not interrupted by update actions (consistency).
% \todo{rimuoverei testo fra parentesi}(that is, an adaptable process can be updated only if $h=0$), 
We write $P(\mathsf{X})$ to denote a process $P$ with zero or more occurrences of process variable $\mathsf{X}$.
Also, 
we write $Q\subst{P}{\mathsf{X}}$ to denote 
the process $Q$ in which free occurrences of $\mathsf{X}$ are substituted with $P$. %---substitution for recursion variables is analogous.
Then, an \emph{update process} $\updated{l}{X}{\INT_1}{\INT_2}{P}$ represents a built-in adaptation mechanism, 
located at $l$.
%able to interact with a located process with abilities $\Delta$, so as to \emph{evolve} to 
%a process with abilities $\Delta'$.
In fact, as explained  below, 
if the \emph{interfaces} of $Q$ and $\INT_1$ are 
\emph{compatible} then 
processes $\component{l}{h}{\INT_1}{Q}$ and $\updated{l}{X}{\INT_1}{\INT_2}{P}$
may interact so as to \emph{evolve} into $Q\subst{P}{\mathsf{X}}$. 
%an adaptable process $\component{l}{h}{\Delta}{P}$. As a result of such interaction, the current content 
%of the adaptable process 
%substitutes all occurrences of $\mathsf{X}$ in 
%(context) $U$, thus resulting in a process $U\subst{P}{\mathsf{X}}$ with abilities $\Delta'$.
Thus, 
intuitively,
process $\updated{l}{X}{\INT_1}{\INT_2}{Q}$ 
behaves as a function which 
expects a process with interface compatible with $\INT_1$ and 
returns an adapted process with interface $\INT_2$.

%in the adaptable process and the map $\Delta_1 \rightarrow \Delta_2$ in the update operator, instead, are used to enable only updates that comply with the map: i.e. an update can occur only if $\Delta = \Delta_1$ thus updating an adaptable processes with the expected capabilities.
% until it synchronizes with an update $\update{l}{X}{\Delta_1 \rightarrow \Delta_2}{U}$. The update replaces the adaptable process $\component{l}{h}{\Delta}{P}$ with the process $U$ where the variable $X$ is substituted with the current state $P$ of the adaptable process -- cfr. Rule $\rulename{r:Upd}$.

%More formally:




%\begin{table}[t]
%$$
%\begin{array}{rcl}
%(\bullet)^{*h}_{\otimes \Delta} & ::= & \bullet \\
%(C \para  P)^{*h}_{\otimes \Delta} & ::= & C^{*h}_{\otimes \Delta} \para  P \\
%(\component{l}{k}{\Delta'}{C})^{*h}_{\otimes \Delta} & ::= & \component{l}{{k*h}}{\Delta'\otimes \Delta}{C^{*h}_{\otimes \Delta}} \\
%(\restr{c}{C})^{*h}_{\otimes \Delta} & ::= & \restr{c}{C^{*h}_{\otimes \Delta}}
%\end{array}
%$$
%\caption{Context update. Above,  $*\in \{+,-\}$  and $ \otimes \in \{\addelta, \midelta \}$.} \label{tab:contextupdate}
%\end{table}


%We usually write $P(\mathsf{X})$ to denote the \emph{(process) context} $P$ with free occurrences of the process variable $\mathsf{X}$.

Binders for the language are as follows: 
channel variable $x$ is bound in 
$\nopenr{a}{x}.P$ and
and $\nopena{a}{x}.P$; similarly, 
$\tilde{x}$ is bound in $\inC{k}{\tilde{x}}.P$ (variables $x_1, \ldots, x_n$ are all distinct). 
%Following~\cite{DBLP:conf/esop/HondaVK98}, given $P$, 
The set of free and bound channels  
and names of a process $P$---noted $\mathsf{fn}(P)$, $\mathsf{fc}(P)$, $\mathsf{bn}(P)$, and $\mathsf{bc}(P)$, resp.
is as expected. 
We define  $\mathsf{fu}(P) \triangleq \mathsf{fn}(P) \cup \mathsf{fc}(P)$.
The treatment of recursion variables is also as customary. 
As for process variables, we assume update processes bind process variables in it. 
In all cases, we rely on usual notions of $\alpha$-conversion (noted $\equiv_\alpha$) and (capture-avoiding) substitution.
We %assume all binders in $\mathsf{open}$ prefixes to be distinct, and 
work only with closed processes.


The semantics of our language is given by 
a \emph{reduction semantics},
denoted $P \pired P'$, the smallest relation on processes generated by the rules in Table~\ref{tab:semantics}.
It relies on  
an evaluation relation on expressions (noted $e \downarrow k$) and on
a structural congruence relation, %noted $\equiv$ and 
 defined as
% (Table~\ref{tab:congruence}). 
the smallest congruence generated by the following laws:
$$
\begin{array}{c}
(P \!\para \! Q) \!\para \! R \!\equiv\! P \!\para \! (Q \!\para \! R) \quad \restr{u}{\component{l}{h}{\Delta}{P}} \!\equiv\! \component{l}{h}{\Delta}{\restr{u}{P}} \quad P \!\para \! \nil \!\equiv\! P  \\ %\quad P \!\equiv\! Q \text{ if } P \!\equiv\!_\alpha Q \\
P \!\para \! Q \!\equiv\! Q \!\para \! P  \quad
\restr{u}{\nil} \!\equiv\! \nil \quad
\restr{u}{\restr{u'}{P}} \!\equiv\! \restr{u'}{\restr{u}{P}} \\
\restr{u}{P} \!\para \! Q \!\equiv\! \restr{u}{(P \!\para \! Q)} ~~\text{(if $u \not\in \mathsf{fu}(Q)$)}   \quad P \!\equiv\! Q \text{ if } P \!\equiv\!_\alpha Q
\end{array}
$$

\begin{table}[t]
$$
%\begin{array}{lr}
%\restr{c}{E\big[C[c(x:\capab).P] \para  D[\outC{c}{v}.R]\big]} \pired & \\
%\quad \restr{c}{E\big[C[P\sub{v}{x}] \para  D[R]\big]} \quad (\text{with } c \in \mathsf{fn}(E,D,C)) & \rulename{r:I/O} \vspace{1.5mm}
%\\
%C[\rec{X:\type{\Phi}{\Delta}}{P} ] \pired C[P\sub{\rec{X:\type{\Phi}{\Delta}}{P}}{X}] & \rulename{r:Rec} \vspace{1.5mm}
%\\
%C[\ifte{v=v}{P}{Q}] \pired C[P] & \rulename{r:IfTr} \vspace{1.5mm}
%\\
%C[\ifte{u=v}{P}{Q}] \pired C[Q]  \quad (\text{with } u \neq v)& \rulename{r:IfFa} \vspace{1.5mm}
%\\
%E\big[C[\component{l}{0}{\Delta_1}{P}] \para  D[\updated{l}{X}{\Delta_1}{\Delta_2}{U}]\big] \pired  & \\
%\quad (E_{\midelta \Delta_1})_{\addelta \Delta_2}\big[(C_{\midelta \Delta_1})_{\addelta \Delta_2}[U\sub{P}{\mathsf{X}}] \para  D[\nil]\big] & \rulename{r:Upd} \vspace{1.5mm}
%\\
%E\big[C[\open{c:\rho}.P] \para  D[\open{d:\overline{\rho}}.R]\big] \pired  & \\
%\quad \restr{c'}{E^{+1}_{\midelta \{\rho, \overline{\rho}\}}\big[{C^{+1}_{\midelta \{\rho\}}[P\sub{c'}{c}] \para  D^{+1}_{\midelta \{\overline{\rho}\}}[R\sub{c'}{d}]}\big]} \quad (\text{with $c'$ fresh}) & \rulename{r:Open} \vspace{1.5mm}
%\\
%\restr{c}{E\big[C[\close{c}.P] \para  D[\close{c}.R]\big]} \pired & \\
%\quad \restr{c}{E^{-1}\big[C^{-1}[P] \para  D^{-1}[R]\big]} & \rulename{r:Close} \vspace{1.5mm}
%\\
%\restr{c}{E\big[C[\branch{c}{n_i:P_i}_{i\in I}] \para  D[\select{c}{n_j}.R]\big]} \pired  & \\
%\quad \restr{c}{E\big[C[P_j] \para  D[R]\big]} & \rulename{r:Branch} \vspace{1.5mm}
%\\
%\text{if } P \equiv P',~ P' \pired Q', \text{ and } Q \equiv Q' ~~\text{then} ~~ P \pired Q & \rulename{r:Str}\vspace{1.5mm}
%\\
%\text{if } P \pired P' ~~\text{then} ~~ \restr{c}{P} \pired \restr{c}{P'} & \rulename{r:Res}
%\end{array}
%%%%%%
\begin{array}{lc}
 \rulename{r:Open} & 
E\big[C[\nopena{a}{x}.P] \para  D[\nopenr{a}{y}.Q]\big] 
\pired  
\restr{\cha}{\big(E^{++}_{}\big[{C^{+}_{}[P\sub{\cha^+}{x}] \para  D^{+}_{}[Q\sub{\cha^-}{y}]}\big]\big)} 
 \vspace{1.5mm}
\\
\rulename{r:I/O} &
E\big[C[\outC{\cha^{\,p}}{\tilde{e}}.P] \para  D[\inC{\cha^{\,\overline{p}}}{\tilde{x}}.Q]\big] 
\pired 
E\big[C[P\sub{\tilde{k}}{\tilde{x}}] \para  D[Q]\big] \quad (\tilde{e} \downarrow \tilde{k}) \vspace{ 1.5mm}
\\
\rulename{r:Upd} & 
E\big[C[\component{l}{0}{}{Q}] \para  D[\updated{l}{X}{\INT_1}{\INT_2}{P}]\big]~~ 
(\text{with }\intf{Q} \compat\INT_1)
\pired   
E_{}\big[C[P\sub{Q}{\mathsf{X}}] \para  D[\nil]\big] \vspace{ 1.5mm}
\\
\rulename{r:Pass} &
E\big[C[\throw{\cha^{\,p}}{\cha'^{\,q}}.P] \para  D[\catch{\cha^{\,\overline{p}}}{x}.Q]\big] \pired E\big[C^{-}[P] \para  D^{+}[Q\sub{\cha'^{\,q}}{x}]\big] \vspace{ 1.5mm}
\\
\rulename{r:Sel} &
E\big[C[\branch{\cha^{\,p}}{n_i:P_i}_{i\in I}] \para  D[\select{\cha^{\,\overline{p}}}{n_j}.Q]\big] 
\pired 
E\big[C[P_j] \para  D[Q]\big]  \quad (j \in I)  \vspace{ 1.5mm}
\\
\rulename{r:IfTr} &
C[\ifte{e}{P}{Q}] \pired C[P]  \quad (e \downarrow \mathtt{true})  \vspace{ 1.5mm}
\\
 \rulename{r:IfFa} &
C[\ifte{e}{P}{Q}] \pired C[Q]  \quad (e \downarrow \mathtt{false}) \vspace{ 1.5mm}
\\
\rulename{r:Close} &
E\big[C[\close{\cha^{\,p}}.P] \para  D[\close{\cha^{\,\overline{p}}}.Q]\big] \pired  E^{-}\big[C^{-}[P] \para  D^{-}[Q]\big] \vspace{ 1.5mm}
\\
 \rulename{r:Str} &
\text{if } P \equiv P',\, P' \pired Q', \,\text{and}\, Q' \equiv Q ~\text{then} ~ P \pired Q \vspace{ 1.5mm}
\\
\rulename{r:Rec} &
C[\rec{Y{:}\ActS{\cdot}\INT}{P} ] \pired C[P\sub{\rec{Y{:}\ActS{\cdot}\INT}{P}}{Y}]  \vspace{ 1.5mm}
\\
 \rulename{r:Res} &
\text{if } P \pired P' ~~\text{then} ~~ \restr{u}{P} \pired \restr{u}{P'} %\vspace{2mm} \\
%\text{\emph{In \rulename{r:Open}, we assume $c'$ is fresh.}} \\
%\text{\emph{In \rulename{r:I/O}, we assume $c \in \mathsf{fn}(E,D,C)$.}}
\end{array}
$$  %\vspace{-4mm}
\caption{Reduction Semantics
%\emph{In $\text{\rulename{r:Sel}}$, $(j \in I)$.}
%\emph{In \rulename{r:I/O}, we assume $c \in \mathsf{fn}(E,D,C)$.}
}\label{tab:semantics}
\end{table}



%Reduction rules  require some additional definitions. 
We write $\pired^{*}$ for the reflexive, transitive closure of $\pired$.
%To represent the fact that 
As processes can be arbitrarily nested inside locations, 
in reduction rules we use  \emph{(syntactic) contexts}, i.e., processes with a \emph{hole} $\bullet$:
$$
C, D, E, \ldots ::= \bullet \sepr \component{l}{h}{\Delta}{C} \sepr C \para  P   
$$
%\todo{toglierei for the sake of space} For the sake of space, w
We assume the expected extension of $\equiv$ 
%structural congruence 
to contexts.
To ensure coherence of located processes along reduction, 
 we define an operation over contexts
 which allows us
%Given $\component{l}{h}{\Delta}{P}$, they allow 
to increase/de\-crease $h$.
%the number of active sessions (given by $h$) 
%and to add/remove types from $\Delta$.
%abilities (given by $\Delta$).
%More precisely, g
Given a context $C$, an integer $j$,
and $* \in \{+,-\}$, %and $ \otimes \in \{\addelta, \midelta \}$, 
we define:
%operations $C^{*j}_{}$ and $C^{}_{\otimes \Delta}$
$$ (\bullet)^{*j}_{}  = \bullet \quad~~ (\component{l}{h}{\Delta}{C})^{*j}_{} = \component{l}{{h*j}}{\Delta}{C^{*j}_{}} \quad~~ (C \para  P)^{*j}_{} = C^{*j}_{} \para  P $$

%$$
%\begin{array}{rclcrcl}
%(\bullet)^{*j}_{} \!\!\!\!\!& ::= & \!\! \bullet \\ % & & (\bullet)^{}_{\otimes \Delta} \!\!\!\!\! & ::= & \!\! \bullet \\
%(\component{l}{h}{\Delta}{C})^{*j}_{} \!\!\!\!\! & ::= & \!\! \component{l}{{h*j}}{\Delta}{C^{*j}_{}} \\ %&  &  \!\! (\component{l}{h}{\Delta'}{C})^{}_{\otimes \Delta} \!\!\!\!\! & ::= & \!\! \component{l}{{h}}{\Delta'\otimes \Delta}{C^{}_{\otimes \Delta}}\\
%(C \para  P)^{*j}_{} \!\!\!\!\! & ::= & \!\! C^{*j}_{} \para  P % & & (C \para  P)^{}_{\otimes \Delta} \!\!\!\!\! & ::= & \!\! C^{}_{\otimes \Delta} \para  P
%%(\restr{c}{C})^{*j}_{} \!\!\!\!\! & ::= & \!\! \restr{c}{C^{*j}_{}} & & \!\!\!\!\!\!\!\!\! (\restr{c}{C})^{}_{\otimes \Delta} \!\!\!\!\! & ::= & \!\! \restr{c}{C^{}_{\otimes \Delta}}
%\end{array}
%$$
%\todo{
%\newcommand{\types}{\mathsf{type}}
%$$
%C_{\otimes \rho} = 
%\begin{cases}
%\bullet & \textbf{if } C= \bullet\\
%\component{l}{h}{\types(C, \rho)}{D_{\otimes \rho}}& \textbf{if } C= \component{l}{h}{\Delta}{D}\\
%D_{\otimes \rho} \para  P& \textbf{if } C= D \para  P
%\end{cases} 
%$$
%where $\types(C, \rho)$ is
%$$
%\types(C, \rho) = 
%\begin{cases}
%\rho & \textbf{if } C= \bullet\\
%l[\types(D,\rho)]& \textbf{if } C= \component{l}{h}{\Delta}{D}\\
%\types(D,\rho) + \quicktype(P) & \textbf{if } C= D \para  P
%\end{cases} 
%$$
%By a slight abuse of notation,
We write ${C}^{-}$ and ${C}^{+}$ to stand for ${C}^{-1}$ and ${C}^{+1}$, resp.
We now comment on rules \rulename{r:Open}, \rulename{r:Close}, and \rulename{r:Upd} in Table~\ref{tab:semantics}; 
other rules are self-explanatory.


%Informally, 
%$\addelta$ (resp. $\midelta$)
%adds (resp. removes) session types from $\Delta$; a formal definition 
% is given in Sect.~\ref{s:types}.
%and write 
%${C}^{*k}_{\otimes \Delta}$ instead of $({C}^{*k})_{\otimes \Delta}$ and $({C}_{\otimes \Delta})^{*k}$.




Rule \rulename{r:Open} formalizes session establishment 
by means of polarized channels, following~\cite{DBLP:journals/acta/GayH05,DBLP:journals/entcs/YoshidaV07}.
%by the interaction of two 
%$\mathsf{open}$ prefixes on the same name and declaring \emph{dual session types} (cf. Def.~\ref{d:dual}).
When a session is initiated, the involved processes are restricted
with a fresh channel $c$; at runtime, each process gets one end of the channel.
%which we assume fresh. %, thus ensuring that channels are unique for each session. 
%This way, channel restriction is only generated at runtime.
Because of session initiation, the number of active sessions 
is increased %by one in 
%the located processes and propagated to 
all enclosing contexts: by one in the context containing the interacting processes, by two in the context enclosing both processes.
%; also, the associated session should be removed from the interfaces of intervening processes. 
%This way, if the two interacting processes are inside a location, the annotations should be updated.
%Hence, in the rule we let 
%$\Delta_1 = \{c:\rho_{\qua}, \, d:\overline{\rho}_{\qua}\}, \Delta_2 = \{c:\rho_{\qua}\}, \Delta_3 \{d:\overline{\rho}_{\qua}\}$.
%These changes are realized with the above operations over contexts. 
%Notice that restriction is not used to build processes but only introduced by the semantics.
Rule \rulename{r:Close} is analogous:
it decreases the active session annotation in 
all enclosing contexts.
Let us write $\intf{P}$ for the \emph{interface} of process $P$ (cf. Sect.~\ref{s:types}). 
Rule \rulename{r:Upd} formalizes update actions. Two conditions are enforced: % which takes place if two conditions are met:
\begin{enumerate}[(1)]
\item Only 
located processes in which 
the number of open sessions is 0 can be updated.
This is to avoid disrupting already established sessions. %update actions which may interrupt session communications.
\item The interface of the located process ($\intf{Q}$) 
and the requirements of the update process ($\INT_1$)
must be \emph{compatible}---noted $\INT_1 \compat \intf{Q}$.
For the sake of simplicity, 
in the remainder we assume $\compat \, \triangleq \, = $.
Sect.\ref{sec:int} discusses more flexible  definitions.
%A simple (but too restrictive) definition is 
%requiring  both interfaces exactly match, i.e., letting $\compat \, \triangleq \, = $.
%%Alternative definitions are discussed later on. %We discuss more interesting forms later on.
%More appealing are notions of compatibility based on \emph{subtyping}~\cite{DBLP:journals/acta/GayH05,DBLP:journals/fuin/VallecilloVR06}.
%Although adding subtyping to our type structure (Sect.~\ref{s:types}) should not pose 
%any difficulties, the thorough treatment of notions of interface compatibility  
%is left for future work.
\end{enumerate}
An update (or evolvability) step  is then realized by 
  substituting $Q$ (the current behavior of the located process) into  $P(\mathsf{X})$.
% is updated and (ii) the annotations for the enclosing context must be adjusted so as to account for the moved interfaces. 
This is a form of \emph{objective update}, as the located process does not 
contain information on future update actions: it reduces autonomously until it is adapted by an  update process in its surrounding context. 







%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%



\section{The Type System}\label{s:types}
Our type discipline builds upon the one given in~\cite{DBLP:conf/ppdp/GarraldaCD06}.
As such, the type syntax is divided into three categories: \emph{basic types}, which  handle expressions; 
\emph{pre-session types} describing a channel's ability for sending/receiving messages and offering/selecting be\-hav\-iors; 
\emph{session types} representing well-formed session-typed be\-hav\-ior. %; and
%\emph{channel types}, which can be a session type or a \emph{used session}~$\bot$. %this will be made clear later on).

We extend the judgments of~\cite{DBLP:conf/ppdp/GarraldaCD06} with an \emph{interface} $\INT$---the collection of all session types declared in a given process. 
As we have seen, interfaces are key to the operational definition of update actions. 
To define the interface of processes with recursion, our 
session types are \emph{qualified}: they can be linear ($\qual$) or unrestricted ($\quau$). 
While $\qual$ is used for those session types to be used just once, 
$\quau$ annotates those session types intended to feature a persistent behavior---roughly, these
are types assigned to sessions declared in the context of a recursive process.
We use $\qua$ to range over $\qual$ and $\quau$.
Formally, we have:

%\end{document}
 
\begin{definition}\label{d:types}
 \emph{Basic types} ($\capab$), \emph{pre-session types} ($\zeta$), and
 \emph{session types} ($\ST_\qua$)
% and \emph{channel types} ($\omega$) 
are as in Table~\ref{tab:types}.
\begin{table}
\textsc{Types}
$$
\begin{array}{lclr}
\capab & ::= & \mathsf{int} \sepr \mathsf{bool} \sepr \dots ~~~& \text{basic types}\\
%\varphi & ::= & \var & \text{process variable \todo{are these used?}} \\
%\end{array}
%$$
%%Session Types 
%$$
%\begin{array}{lcll}
\zeta &\!\!\!\!::= & \epsilon \!\!\!\!\!\!& \text{closed session}\\
		& \sepr &  !(\tilde{\capab}).\zeta \sepr ?(\tilde{\capab}).\zeta & \text{send, receive} \\ 
		& \sepr &  !(\sigma).\zeta \sepr ?(\sigma).\zeta & \text{throw, catch} \\ 
		& \sepr &  t & \text{type variable} \\ 
		& \sepr &  \mu t.\zeta & \text{recursive type} \\ 
		& \sepr &  \&\{n_1:\zeta_1, \dots,  n_k:\zeta_k \}  \quad &  \text{branch} \\
		& \sepr &  \oplus\{n_1:\zeta_1, \dots , n_k:\zeta_k \}  &  \text{select} \vspace{0.5mm} \\
\qua &\!\!\!\!::= & \!\!\!\qual \sepr \quau \!\!\!\!\!\!& \text{type qualifiers} \vspace{0.5mm} \\
\ST_\qua & \triangleq & \!\!\!\!\ \{ \zeta ~|~ \mathsf{ftv}(\zeta) = \emptyset\} & \text{session type} \vspace{0.5mm}\\
%\end{array}
%. \\
%\begin{array}{lcll}
%~\omega &::=& \ST_\qua & \text{session types}\\
%	& \sepr &	\bot \quad& \text{used session}
\end{array}
$$
\textsc{Environments}
$$
\begin{array}{lclr}
\INT &\!\!\!::= &  \emptyset \sepr \INT, \langle \ST, k \rangle \sepr \INT ,  \langle \cha:[\ST_\qua], 1 \rangle& \text{process interface} \\
\ActS & ::= &  \emptyset \sepr \ActS , k:\ST_\qua  & \text{active sessions}\\
\Gamma &::= &  \emptyset \sepr \Gamma, e:\capab \sepr \Gamma, a:\langle \ST_\qua , \overline{\ST_\qua} \rangle & \text{first-order env.}\\
\Theta &::= &  \emptyset \sepr \Theta, Y:\ActS{\cdot}\INT \sepr \Theta,\mathsf{X}:\INT \quad& \text{higher-order env.}
\end{array}
$$  %\vspace{-4mm}
\caption{Types and Typing Environments}\label{tab:types}
\end{table}
\end{definition}

Our type syntax contains the usual session types constructs, with 
their standard meanings. 
We use $t, t', \ldots$ to range over \emph{type variables}; also, we 
require recursive types to be \emph{contractive}, i.e., not 
containing a subexpression of the form $\mu t.\mu t_1.\cdots.\mu t_n.t$.
Binder $\mu$ gives rises to standard notions of free/bound type variables; 
$\mathsf{ftv}(\zeta)$ denotes the free type variables in $\zeta$.
We consider session types modulo folding/unfolding of recursive types.
%\todo{contractive types?}
We now introduce the central notion of  \emph{duality} for (pre-session) types.


\begin{definition}[duality]\label{d:dual}
Given a pre-session type $\zeta$, 
its \emph{dual}
(noted $\overline{\zeta}$) is inductively defined in Table~\ref{tab:dual}.
\begin{table}[t]
$$
\begin{array}{rcl}
 \overline{\epsilon} & =  & \epsilon\\
 \overline{!(\tau).\zeta} & =  & ?(\tau).\overline{\zeta} \text{~~(with $\tau = \tilde{\capab}$ or $\tau = \ST_\qua$)}\\
 \overline{?(\tau).\zeta} & =  & !(\tau).\overline{\zeta} \text{\,~~(with $\tau = \tilde{\capab}$ or $\tau = \ST_\qua$)}\\
% \overline{?(\tau).\zeta} &\!\!=\! & !(\tilde{\capab}).\overline{\zeta}\\
% \overline{!(\sigma).\zeta} &\!\!=\! & ?(\sigma).\overline{\zeta}\\
% \overline{?(\sigma).\zeta} &\!\!=\! & !(\sigma).\overline{\zeta}\\
 \overline{t} &\!\!=\! & t \\
 \overline{\mu t.\zeta} &\!\!=\! & \mu t.\overline{\zeta}\\
 \overline{\&\{n_1:\zeta_1 , \ldots , n_k:\zeta_k \}} &\!\!=\! & \oplus\{n_1:\overline{\zeta_1} , \ldots , n_k:\overline{\zeta_k} \}\\
 \overline{ \oplus\{n_1:\zeta_1 , \ldots , n_k:\zeta_k \}} &\!\!=\!& \&\{n_1:\overline{\zeta_1} , \ldots , n_k:\overline{\zeta_k} \}
\end{array}
$$ %\vspace{-4mm}
\caption{Dual of pre-session types}\label{tab:dual}
\end{table}
\end{definition}

%In order to type a process $P$ 
%We use two kinds of typing environments, noted $\Gamma$ and $\Theta$.
We comment on the typing environments defined in Table~\ref{tab:types}.
An interface $\INT$ is a set of pairs $\langle \ST, k\rangle$ where $\ST$
is a session type and $k$ is either an integer $j > 0$ or $\infty$.
The intention is to capture the session types declared in a process,
the number of times a type is declared, and whether a type is 
%declared in the context of a recursive definition.
%\todo{I would substitute the above sentence with: and whether a type is 
linear or unrestricted.
In $\INT$, types are recorded at most once; several occurrences of the same type are captured
by the second component of the pair. 
The union of an interface and a pair,
noted $\INT \addelta \langle \ST, k\rangle$, is defined as follows:
$$
\INT \addelta \langle \ST, k\rangle \!\triangleq \!\!
\begin{cases}
\INT' \cup \{\langle \ST, k + j\rangle \} & \text{if } \exists\INT'. \,  \INT = \INT' \cup \{\langle \ST, j\rangle \}	\\
\INT \cup \{\langle \ST, k \rangle \} & \text{otherwise} 
\end{cases}
$$
Recall that $\infty + 1 = \infty$.
We sometimes write $\INT \addelta \ST_\qua$ to stand 
for $\INT \addelta\{\langle \ST, 1\rangle \}$ (if $\qua = \qual$) or
$\INT \addelta \{\langle \ST, \infty\rangle \}$ (if $\qua = \quau$).
The extension of $\addelta$ from pairs $\langle \ST, k \rangle$ 
to interfaces (denoted $\INT_1 \addelta \INT_2$) is as expected.
Letting $\pi$ stand for \emph{session prefixes} (expression/channel input and output, session selection and close), 
the interface of a process $P$, denoted $\intf{P}$, is inductively defined in Table~\ref{tab:int}.

\begin{table}[ht]
$$
\intf{P} =  
\begin{cases}
\langle \ST,1 \rangle \addelta \intf{P'}& \text{if } P = \nopena{a}{x:\ST_\qual}.P'\text{ or }P = \nopenr{a}{x:\ST_\qual}.P' 	\\
\langle \ST,\infty \rangle \addelta \intf{P'} & \text{if } P = \nopena{a}{x:\ST_\quau}.P'\text{ or }P = \nopenr{a}{x:\ST_\quau}.P' 	\\
\intf{P'} & \text{if } P = \component{l}{h}{\a}{P'} \text{ or } P = \pi.P' \\
\emptyset & \text{if } P = \updated{l}{X}{\INT_1}{\INT_2}{Q} \text{ or } P = \mathbf{0} \\
\intf{P_1} & \text{if } P = \ifte{e}{P_1}{P_2} \\
\INT& \text{if } P = \rec{Y{:}\ActS{\cdot}\INT}{P'}\\	
\intf{P_1} \addelta \intf{P_2}\!\!\!\!& \text{if } P = P_1 \para  P_2 \\	 
\biguplus_i(\intf{P_i}) & \text{if } P = \branch{c}{n_1{:}P_1, \ldots, n_k{:}P_k} \\
\intf{P'} & \text{if } P = \restr{c}{P'} 
\end{cases}
%\vspace{-4mm}
$$
\caption{Interface of a process $P$}\label{tab:int}
\end{table}

Set $\ActS$ collects information on already active sessions: it records 
a channel name %on which the communication is taking place and the 
and its associated session type. % $\rho$ associated to the channel.  
While $\Gamma$ is a first-order environment which maps expressions with basic types $\capab$,
the higher-order environment $\Theta$ stores the type of process/recursion variables.
%%\todo{Add here that we consider update variables $\mathsf{X}$ and recursion variables $X$; we use $\mathcal{X}$ to refer to one of them.}
%The type of a process is divided into two parts, noted $\Phi$ and $\Delta = \Delta_l \shortmid \Delta_u$, resp.
%
%We use $\Delta_l \shortmid \Delta_u $ to denote information on the interface: i.e., what sessions can be established along the evolution of a process. This notation is intended to distinguish between \emph{linear} and \emph{unrestricted} sessions:
%while the set $\Delta_u$ will contain all those sessions which are in the scope of a recursion operator, 
%all the other sessions are linear and thus accumulated in the multiset $\Delta_l$. 
%
%We assume an operator $\addelta$ which adds sessions to  $\Delta_u$ and  $\Delta_l$ depending on the nature of each zone:  
%an unrestricted session is added only if it is not already present, 
%while a linear session is always added (as it is a multiset). 
%Dually, operator $\midelta$ is used to remove sessions from $\Delta_u$ and  $\Delta_l$: 
%while a removal from $\Delta_u$ has no effect, we write $\Delta_u \midelta \rho$ to denote the removal of one occurrence of session $\rho$ from $\Delta_l$. 
%\todo{Q: These operators are defined over sessions or over sets of sessions??}
%In what follows, to simplify the notation, we often write $\Delta$ to stand for $\Delta_l \shortmid \Delta_u $.
%Here we present the type system for our process language.
Given these environments, a \emph{type judgment} is  of form
$$\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}} $$ 
meaning that, under environments $\Gamma$ and $\Theta$, 
process $P$ has active sessions declared in $\ActS$ and interface %(a collection of not yet open sessions) 
$\INT$. We then have:

\begin{definition}%[Well-typed process]
A process is well-typed if it can be typed using the rules in Tables \ref{tab:pitype} and~\ref{tab:session}.
\begin{table}[h!]

$$
\begin{array}{cr}

\cfrac{}{\Gamma \vdash e:\capab} \quad \cfrac{}{\Gamma, x:\capab \vdash x:\capab} \quad \cfrac{}{\Gamma; \Theta,\mathsf{X}:\INT \vdash \mathsf{X}:\type{\emptyset}{\INT}} & \rulename{t:Exp},  \rulename{t:NVar}, \rulename{t:PVar}\\

%\cfrac{}{\Gamma, x:\capab \vdash x:\capab} & \rulename{t:NVar} \vspace{-1mm}\\

%\cfrac{}{\Gamma; \Theta,\mathsf{X}:\INT \vdash \mathsf{X}:\type{\emptyset}{\INT}}  & \rulename{t:PVar} \vspace{-1mm}\\



 \cfrac{}{\Gamma; \Theta,X:\ActS{\cdot}\INT \vdash X:\type{\ActS}{\INT}} \quad \cfrac{}{\judgebis{\env{\Gamma}{\Theta}}{\nil}{\type{\emptyset}{\emptyset}}}&  \rulename{t:RVar}, \rulename{t:Nil}  \vspace{2.5mm}\\

%\cfrac{
%\begin{array}{c}
%\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\ST_\qua}{\,\INT}} 
%%\mathsf{cond}(\INT, \INT_l, \INT_u,  \Theta, \rho)
%\end{array}
%}{\judgebis{\env{\Gamma}{\Theta}}{\nopen{a}{x:\ST_\qua}.P}{ \type{\ActS , x:\ST_\qua}{\,\INT \addelta \ST_\qua}}} & \rulename{t:Open} \vspace{2.5mm} 
%\\
%
%
%\cfrac{
%\Gamma \vdash a: \langle \ST_\qua , \overline{\ST_\qua } \rangle \quad
%\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\ST_\qua}{\,\INT}} 
%}{\judgebis{\env{\Gamma}{\Theta}}{\nopen{a}{x}.P}{ \type{\ActS , x:[\ST_\qua]}{\,\INT \addelta \ST_\qua}}} & \rulename{t:IdeaOpen} \vspace{2.5mm} 
%\\

\cfrac{
\Gamma \vdash a: \langle \ST_\qua , \overline{\ST_\qua } \rangle \quad
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\ST_\qua}{\,\INT}} 
}{\judgebis{\env{\Gamma}{\Theta}}{\nopena{a}{x}.P}{ \type{\ActS}{\,\INT \addelta x: \ST_\qua}}} 
& 
\rulename{t:Accept} \vspace{2.5mm} 
\\
\quad 
\cfrac{
\Gamma \vdash a: \langle \ST_\qua , \overline{\ST_\qua } \rangle \quad
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\overline{\ST_\qua }}{\,\INT}} 
}{\judgebis{\env{\Gamma}{\Theta}}{\nopenr{a}{x}.P}{ \type{\ActS}{\,\INT \addelta x: \overline{\ST_\qua }}}} 
& 
%\rulename{t:Accept} 
\rulename{t:Request} \vspace{2.5mm} 
\\

\cfrac{\judgebis{\env{\Gamma, \tilde{x}:\tilde{\capab}}{\Theta}}{P}{\type{\ActS, k:\ST}{\INT}}}{\judgebis{\env{\Gamma}{\Theta}}{\inC{k}{\tilde{x}}.P }{\type{\ActS, k:?(\tilde{\capab}).\ST}{ \INT}}}
\quad
\cfrac{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\ST}{ \INT}} \qquad \Gamma \vdash \tilde{e}:\tilde{\capab}}{\judgebis{\env{\Gamma}{\Theta}}{\outC{k}{\tilde{e}}.P}{\type{\ActS, k:!(\tilde{\capab}).\ST}{ \INT}}} & \rulename{t:In}, \rulename{t:Out}  \vspace{2.5mm}
\\


\cfrac{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\STT}{ \INT}}}{\judgebis{\env{\Gamma}{\Theta}}{\throw{k}{k'}.P}{\type{\ActS, k:!(\ST).\STT, k':\ST}{ \INT}}} 
\quad
\cfrac{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\STT, x:\ST}{\INT}}}{\judgebis{\env{\Gamma}{\Theta}}{\catch{k}{x}.P }{\type{\ActS, k:?(\ST).\STT}{ \INT}}}
& \rulename{t:Thr}, \rulename{t:Cat}  \vspace{2.5mm}
\\



\cfrac{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}} \qquad h = \#\{k \mid k:\ST_\qua \in \ActS\} + \#\{\cha \mid \cha:[\ST_\qua] \in \INT\} }{\judgebis{\env{\Gamma}{\Theta}}{\component{l}{h}{\INT}{P} }{ \type{\ActS}{\INT}}} &  \rulename{t:Loc}  \vspace{2.5mm}
\\

\cfrac{\judgebis{\env{\Gamma}{\Theta,\mathsf{X}:{\INT_1}}}{P}{\type{\emptyset}{ \INT_2 }}}{\judgebis{\env{\Gamma}{\Theta}}{\updated{l}{X}{\INT_1}{\INT_2}{P}}{\type{\emptyset}{ \emptyset}}} & \rulename{t:Upd}  \vspace{2.5mm}
\\ 

%\cfrac{
%\begin{array}{l}
%\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1}{ \INT_1}} \\
% \judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS_2}{ \INT_2}}
%\end{array}
% \quad 
%\begin{array}{l}
%\ActS = \ActS_1 \bowtie \ActS_2 \\ \INT = \INT_1 \addelta \INT_2
%\end{array}}{\judgebis{\env{\Gamma}{\Theta}}{P \para  Q}{\type{\ActS}{\INT}}} & \rulename{t:Par}  \vspace{2.5mm}
%\\


\cfrac{
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1}{ \INT_1}} \qquad
 \judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS_2}{ \INT_2}}
 \qquad
%\ActS = \ActS_1 \bowtie \ActS_2 \\
 \INT = \INT_1 \addelta \INT_2}{\judgebis{\env{\Gamma}{\Theta}}{P \para Q}{\type{\ActS_1, \ActS_2}{\INT}}} & \rulename{t:Par}  \vspace{2.5mm}
\\

%\cfrac{\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS, c:\bot }{ \INT}}}{\judgebis{\env{\Gamma}{\Theta}} {\restr{c}{P}}{\type{\ActS, c:\bot}{ \INT}}}
%
%& \rulename{t:CRes} \vspace{2.5mm}



%\cfrac{\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS, c^-:\ST, c^+:\overline{\ST} }{ \INT}}}{\judgebis{\env{\Gamma}{\Theta}} {\restr{c}{P}}{\type{\ActS, c^-:[\ST], c^+:[\overline{\ST}]}{ \INT}}} 
\cfrac{\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS, \cha^-:\ST, \cha^+:\overline{\ST} }{ \INT}}}{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}}{\type{\ActS}{ \INT, \cha^-:[\ST], \cha^+:[\overline{\ST}]}}} 

\qquad
\cfrac{\judgebis{\env{\Gamma \cdot a : \langle \ST, \overline{\ST} \rangle }{\Theta}}{P }{\type{\ActS }{ \INT \cdot \ST \cdot \overline{\ST} }}}{\judgebis{\env{\Gamma}{\Theta}} {\restr{a}{P}}{\type{\ActS}{ \INT}}} 

& \rulename{t:CRes}, \rulename{t:NRes} \vspace{2.5mm}
\\
%\cfrac{\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS, c^-:\ST, c^+:\overline{\ST} }{ \INT}}}{\judgebis{\env{\Gamma}{\Theta}} {\restr{c}{P}}{\type{\ActS}{ \INT, [c^-:\ST], [c^+:\overline{\ST}]}}} 
%
%& \rulename{t:Idea2CRes} \vspace{2.5mm}
%\\



\cfrac{ \judgebis{\env{\Gamma}{\Theta,Y:\ActS{\cdot}\INT}}{ P}{\type{\ActS}{\INT}}}{\judgebis{\env{\Gamma}{\Theta}}{\rec{Y:\ActS{\cdot}\INT}{P}}{\type{\ActS}{\INT}}} & \rulename{t:Rec} \vspace{2.5mm}
\\


 
 \cfrac{\judgebis{\env{\Gamma}{\Theta}}{ P}{\type{\ActS}{\INT}} \qquad k\notin \dom{\ActS} }{\judgebis{\env{\Gamma}{\Theta}}{ \close{k}.P}{ \type{\ActS, k:\epsilon}{ \INT}}} & \rulename{t:Clo}
\end{array}
$$ % \vspace{-4mm}
\caption{Well-typed processes (I) }\label{tab:pitype}
\end{table}



\begin{table}[ht]

$$
\begin{array}{cr}



\cfrac{
\begin{array}{l}
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}} \qquad
\judgebis{\env{\Gamma}{\Theta}}{Q}{\type{\ActS}{\INT}}
\end{array}
 \quad 
 \Gamma \vdash e:\mathsf{bool} 
 }{\judgebis{\env{\Gamma}{\Theta}}{\ifte{e}{P}{Q}}{\type{\ActS}{\INT}}} & \rulename{t:If} 
 \vspace{2.5mm}
 \\
%\end{array}
%$$
%
%\caption{Well-typed located and update processes.}\label{tab:update}
%\end{table}
%
%
%\begin{table}[t]
%
%
%
%$$
%\begin{array}{cr}

%\cfrac{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, c:\rho}{ \INT}} \quad \INT' = \begin{cases}
%\INT_u \addelta \rho & X \in \Theta\\
%\INT_l \addelta \rho & \text{otherwise}
%\end{cases}
%}{\judgebis{\env{\Gamma}{\Theta}}{\open{c:\rho}.P}{ \type{\ActS}{\INT'}}} & \rulename{Open}\\

\cfrac{\judgement{\Gamma}{\Theta}{P}{\ActS}{\INT} \qquad c\notin \dom{\ActS} }{\judgement{\Gamma}{\Theta}{\restr{c}{P}}{\ActS}{\INT}} & \rulename{t:Weak} \vspace{2.5mm}
\\

\cfrac{
\begin{array}{c}
\forall i\in \{1,\ldots, k\}. \judgebis{\env{\Gamma}{\Theta}}{P_i}{\type{\ActS, c:\ST_i}{ \INT}} \qquad
 \ST = \&\{n_1:\ST_1,\ldots, n_k:\ST_k \}
\end{array} 
 }{\judgebis{\env{\Gamma}{\Theta}}{\branch{c}{n_1:P_1, \ldots, n_k:P_k}}{\type{ \ActS, c:\ST}{ \INT}}} & \rulename{t:Bra} \vspace{2.5mm}
\\

\cfrac{
\begin{array}{c}
\judgebis{ \env{\Gamma}{\Theta}}{P}{\type{\ActS, c:\ST_i}{ \INT}} \quad 1 \leq i \leq k \qquad
\ST = \oplus\{n_1:\ST_1, \ldots , n_k:\ST_k \}
\end{array}
}{\judgebis{\env{\Gamma}{\Theta}}{\select{c}{n_i}.P}{\type{\ActS, c:\ST}{\INT}}} & \rulename{t:Sel}
\end{array} % \vspace{-4mm}
$$
\caption{Well-typed processes (II)}\label{tab:session}
\end{table}
\end{definition}







We comment on some typing rules. %, starting with those rules which handle sessions (Table~\ref{tab:session}). 
Rule \rulename{t:Open} types the process $\nopen{a}{x:\ST_\qua}.P$. 
Observe how channel $c$
becomes bound and so it is removed from $\ActS$; 
simultaneously, 
$\INT$ is extended with 
the now complete (non-active) session $\ST_\qua$.
%To enforce the distinction between $\Delta_u$ and $\Delta_l$ explained above, in 
%that rule,  $\mathsf{cond}(\Delta, \Delta_l, \Delta_u,  \Theta, \rho)$ stands for the predicate
%$(\exists X. X \in \dom{\Theta} \land \Delta = (\Delta_u \addelta \rho \shortmid \Delta_l)) \lor (\Delta = (\Delta_u \shortmid \Delta_l \addelta \rho))$.
%$(\Theta \neq \emptyset \land \Delta = (\Delta_u \addelta \rho \shortmid \Delta_l)) \lor (\Delta = (\Delta_u \shortmid \Delta_l \addelta \rho))$.
%Hence, if the session appears in the scope of a recursive operator (and so at least one recursion variable is declared in $\Theta$), then $\rho$ is added to  $\Delta_u$, otherwise it is inserted in $\Delta_l$.
Rule \rulename{t:Loc} checks that $h$ corresponds to the number of running sessions in $P$, i.e., the cardinality of $\ActS$.
Rule \rulename{t:Upd} requires that the type of $P(\mathsf{X})$ is $\INT_2$ provided that $\mathsf{X}$ is of type ${\INT_1}$. 
This way, the rule guarantees that the process resulting from an update action has the declared interfaces. 
%We also require that no active session is present in  $P(\mathsf{X})$.
%Finally, rules in Table \ref{tab:pitype}
%are used  to type  usual $\pi$-calculus and are standard. We comment only on 
Rule \rulename{t:Par} puts processes in parallel. 
%This is obtained via the \emph{merge operator} $\bowtie$, which ensures 
%session type compatibility via duality:
%
%
%\begin{definition}%[Merge]
%We define 
%$\omega_1 \bowtie \omega_2 = \bot$ if $\{\omega_1, \omega_2\} = \{ \ST , \overline{\ST}\}$
%and $\omega_1 \bowtie \omega_2\,=\,\text{undefinded}$ otherwise. Then:
%$$
%\begin{array}{lcl}
%\ActS_1 \bowtie \ActS_2 &\!\! =\!\!& \{ c:\omega_1 \bowtie \omega_2 \mid c:\omega_1 \in \ActS_1 \text{ and } c:\omega_2 \in \ActS_2\} \;\cup \\
%&&\{ c:\omega_1 \mid c:\omega_1 \in \ActS_1 \text{ and } c\notin \dom{\ActS_2}\} \;\cup\\
%&&\{ c:\omega_2 \mid c:\omega_2 \in \ActS_2 \text{ and } c\notin \dom{\ActS_1}\}
%\end{array}
%$$
%\end{definition}
Rule \rulename{t:Close} extends $\ActS$ with a new channel with an empty session type. %whose associated session is still empty.
Rules \rulename{t:PVar} and \rulename{t:RVar} handle process and recursion variables, resp. %In both cases, they define an empty $\Phi$.
Rule \rulename{t:Weak} handles all those processes in which $\restr{c}{P} \equiv P$ holds, and %, i.e., where $c$ does not occur in $P$.
\rulename{t:CRes} types channel restriction (the expected rule for name restriction is elided).
%Rules in Table \ref{tab:update} are used to type adaptable processes and update actions. In particular, notice that 
While rules \rulename{t:Cat} and \rulename{t:Thr} handle delegation,
rules \rulename{t:In}, \rulename{t:Out},  
%\rulename{t:Cat}, \rulename{t:Thr},
\rulename{t:Bra},  and \rulename{t:Sel} are standard.
%they extend an existing session with the proper type.  

%\todo{dire che altre regole sono standard?}
%\todo{Rule \rulename{Rec} not sure what to write for rec}



%\section{Varius Comments}
%\begin{enumerate}
%	
%	\item pensare se il calcolo avrebbe piu' o meno senso, impedendo di eliminare locations	
%	
%	\item ATTENZIONE la regola \rulename{Loc red} crea un problema: se inclusa si rischia di non aggiornare le sessioni aperte al momento di una open (e simmetricamente di non chiuderle in caso di una close) questo comporta che in tutte le reduction rules ci si debba ricordare il nesting delle location fino a top level (ruolo di E), da questa osservazione deriva anche la giustificazione della definizione di nesting context
%	$$
%	\cfrac{P \pired P' }{\component{l}{n}{}{P} \pired \component{l}{n}{}{P'}} \qquad \rulename{Loc red}\\
%	$$
%
%	
%\end{enumerate}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newpage
\section{A More Flexible Typing System}

\input{newtype}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\section{Session Consistency by Typing}\label{sec:res}
\input{consistency}

We now investigate \emph{session consistency}: this is to 
%address a basic consequence of considering
enforce a basic discipline on 
the interplay of communicating behavior (i.e., session interactions) 
and evolvability behavior (i.e., update actions). 
We say that sessions are \emph{consistent} when they are not disrupted by an evolvability step. 
That is, performing an update action does not affect the behavior of active sessions.
To define consistency, we extend and adapt  notions 
given in~\cite{DBLP:conf/ppdp/GarraldaCD06}. %\todo{Do we also distinguish between pre- and processes?}
Process $P$ is said to be \emph{communicating} over channel $c$ if it is one of the following:
$$
\begin{array}{llcllcrl}
(1)  &  \inC{c^{\,p}}{\tilde{x}}.P' & & (2) & \outC{c^{\,p}}{v}.P' & & \!\!\!  (7) &   \close{c^{\,p}}.P'  \\
(3)  &   \catch{c^{\,p}}{x}.P' & & (4) &    \throw{c^{\,p}}{d^{\,q}}.P' \\
(5)  &   \branch{c^{\,p}}{n_1{:}P_1, \ldots, n_k{:}P_k} ~~ & & (6)  &   \select{c^{\,p}}{n}.P' 
\end{array}
$$
Two communicating processes are \emph{dual} %of each other 
(on session $c$)
if they are, respectively, of the forms (1) and (2), 
(3) and (4), 
(5) and (6),
or a pair of (7), as given above.
Let us write $P_{\langle c \rangle}$ and $\overline{P}_{\langle c \rangle}$ for two dual communicating processes on $c$.
Below, let $\pired_r$ stand for an update action, i.e., 
a reduction inferred using rule $\rulename{r:Upd}$, possibly preceded/followed
by uses of rules $\rulename{r:Res}$/$\rulename{r:Str}$. 
We define:

\begin{definition}[Consistency]\label{d:consist}%
A session on channel $c$ is \emph{consistent} in a process $P$ if,
for all $P', P''$ such that 
$$P \pired^{*} P' \equiv (\nu \tilde{u})\big (E\big[C[Q_{\langle c \rangle}] \para  D[\overline{Q}_{\langle c \rangle}]\big] \big)$$
%where $R$ and $Q$ are dual communicating processes in that session, 
and $P' \pired_r P''$, then there exist contexts $E', C'$, and $D'$ such that
$P'' \equiv (\nu \tilde{u})\big (E'\big[C'[Q_{\langle c \rangle}] \para  D'[\overline{Q}_{\langle c \rangle}]\big]\big)$.
\end{definition}

Hence, intuitively, Def.~\ref{d:consist} formalizes the fact that
reductions corresponding to update actions do not disrupt the behavior of communicating processes
in already active sessions. They can only involve parts of the system not engaged into active sessions.

We can show that all sessions in our well-typed processes are consistent. 
This result follows as a direct consequence of the \emph{subject reduction} theorem below: i.e., well-typedness is preserved by reduction.
Its proof relies on a subject congruence result, and on a result on typability of processes within (syntactic) contexts $C$.
%(see the Appendix for a  detailed proof). 

%\todo{The statement below can be simplified to three cases (merging 2 and 3). Do we define substitution over $\Delta$? Also, I think we need subject congruence.}

%\end{document}

\begin{theorem}[Subject Congruence] \label{th:congr}
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$ and $P \equiv Q$ then $\judgebis{\env{\Gamma}{\Theta}}{Q}{\type{\ActS}{\INT}}$.
\end{theorem}
\begin{proof}
By induction on the derivation of $P \equiv Q$, with a case analysis on the last applied rule.
%The proof proceeds by a case analysis on the structural rule applied to obtain the congruence. 
TO DO! \\
We should detail at least case $\restr{u}{\component{l}{h}{\Delta}{P}} \!\equiv\! \component{l}{h}{\Delta}{\restr{u}{P}}$ ($u$ is either a channel or a name. this seems to work both when $u$ is a channel $c$ and when it is a name $a$).
\qed
\end{proof}

%Below we write $\ActS \sim \ActS'$ whenever 
%$\ActS, \ActS'$ 
%are equal OR 
%whenever they differ only on bracketed assignments, as follows:
%%$\ActS, \ActS'$ have exactly the same unbracketed assignments $c:\ST$,
%%and contain the same unbracketed types, possibly on different names.
%%That is, 
%$\ActS \sim \ActS'$ holds when (a) both $\ActS, \ActS'$ are empty;
%(b) if for every $c: \ST$ there are $\ActS'_1, \ActS_1$ such that $\ActS = \ActS_1 \cdot c:\ST, \ActS' = \ActS'_1 \cdot  c:\ST$
%and $\ActS_1 \sim \ActS'_1$;
%(c) if for every $[\ST]$ there are $\ActS'_1, \ActS_1, c, d$ such that $\ActS = \ActS_1 \cdot c:[\ST], \ActS' = \ActS'_1 \cdot  d:[\ST]$
%and $\ActS_1 \sim \ActS'_1$.

Subject reduction works for balanced envionments; we need to introduce that notion.

\begin{theorem}[Subject Reduction]\label{th:subred}
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$ and $P \pired Q$ then 
%one of the following holds: \vspace{-2mm}
either:
\begin{enumerate}[(1)]
% \item $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\Phi}{\Delta}}$;
% \item $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\Phi}{\Delta\sub{v}{x}}}$;
%  \item $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\Phi}{\Delta'}}$ for some $\Delta'$
%  \item $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\Phi, c:\bot}{\Delta\ominus\{\rho, \overline{\rho}\}}}$ for some $\rho$;
 \item $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS}{\INT}}$; %\vspace{-2mm}
  \item $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS}{\INT'}}$, for some $\INT'$. %\vspace{-2mm}
%  \item $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS, c:\bot}{\INT'}}$, for some $\INT' \subset \INT$ and channel $c$.
\end{enumerate}
\end{theorem}


\begin{proof}
We assume that $\tilde{e} \downarrow \tilde{k}$ is a type preserving operation, for every $\tilde{e}$.
The proof proceeds by induction on the rule applied in the reduction. 
%Lemma \ref{lem:context} allows us to consider  only the partners involved in the reduction regardless of the contexts where those process appear.
\begin{description}
\item[Case \rulename{r:Open} - idea]
Suppose $\judgebis{\env{\Gamma}{\Theta}}{\nopen{a}{x:\ST_\qua}.P_1 \para  \nopen{a}{y:\overline{\ST_\qua}}.P_2}{\type{\ActS}{\INT}}$. This
assumption is derived using rule \rulename{t:IdeaOpen} twice, as follows: 
$$
\frac
{\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\ActS_1, x:\ST_\qua}{\,\INT_1}} }
{\judgebis{\env{\Gamma}{\Theta}}{\nopen{a}{x}.P_1}{ \type{\ActS_1,}{\,\INT_1 \addelta x:\ST_\qua}}}
\quad
\frac
{\judgebis{\env{\Gamma}{\Theta}}{P_2}{\type{\ActS_2, y:\overline{\ST_\qua}}{\,\INT_2}} }
{\judgebis{\env{\Gamma}{\Theta}}{\nopen{a}{y}.P_2}{ \type{\ActS_2 }{\,\INT_2 \addelta  y:\overline{\ST_\qua}}}}
$$
where $\ActS = \ActS_1, \ActS_2, $ and $\INT = \INT_1, \INT_2 \addelta \{x: \ST_\qua,y:\overline{\ST_\qua}\}$.

Now, applying a substitution lemma (yet to be shown) on premises $P_1$ and $P_2$ we have
$$
\judgebis{\env{\Gamma}{\Theta}}{P_1[c^{-}/x]}{\type{\ActS_1, c^{-}:\ST_\qua}{\,\INT_1 }} 
\qquad 
\judgebis{\env{\Gamma}{\Theta}}{P_2[c^{+}/y]}{\type{\ActS_2, c^{+}:\overline{\ST_\qua}}{\,\INT_2 }} 
$$
Then, using rule \rulename{t:IdeaPar}, we have:
$$
\judgebis{\env{\Gamma}{\Theta}}{P_1[c^{-}/x] \para P_2[c^{+}/y]}{\type{\ActS, c^{-}:\ST_\qua, c^{+}:\overline{\ST_\qua}}{\,\INT_1, \INT_2}} 
$$
Now, using rule \rulename{t:Idea2CRes}, we hide session types via brackets, and obtain
$$
\judgebis{\env{\Gamma}{\Theta}}{(\nu c)(P_1[c^{-}/x] \para P_2[c^{+}/y])}{\type{\ActS}{\,\INT_1, \INT_2 \uplus  c^{-}:[\ST_\qua] \uplus c^{+}:[\overline{\ST_\qua}] }} 
$$
%which is \emph{almost} what we want, in the sense that there is a discrepancy on the names for bracketed session types after the reduction ($x$ vs. $c^-$, $y$ vs. $c^+$).
and so we are done, because we fall into item (2), because part of $\INT$ gets bracketed/renamed.\\

	\item[Case \rulename{r:Open}]
We have that $P \equiv \nopen{a}{c:\rho}.P_1 \para  \nopen{a}{d:\overline{\rho}}.P_2$. 
From Lemma \ref{lem:types}(\ref{types1} and \ref{types8}) we have that there exist $\Phi_1, \Phi_2, \Delta_1$ and $\Delta_2$ such that $\Phi = \Phi_1,  \bowtie \Phi_2$,  $\Delta = \Delta_1 \uplus \Delta_2$, 
\begin{itemize}
\item $\judgement{\Gamma}{\Theta}{P_1}{\Phi_1, c:\rho}{\Delta_1 \ominus \rho} $ 
\item $\judgement{\Gamma}{\Theta}{P_2}{\Phi_2, d:\overline{\rho}}{\Delta_2 \ominus \overline{\rho}}$. 
\end{itemize}

Now from Lemma \ref{lem:substitution} (1), we have:
\begin{itemize}
\item $\judgement{\Gamma}{\Theta}{P_1\sub{c'}{c}}{\Phi_1,c':\rho}{\Delta_1 \ominus \rho}$
\item $\judgement{\Gamma}{\Theta}{ P_2\sub{c'}{d}}{\Phi_2,c':\overline{\rho}}{\Delta_2 \ominus \overline{\rho}}$.
\end{itemize}

By means of typing rule \rulename{Par} we obtain  
$$\judgement{\Gamma}{\Theta}{ P_1\sub{c'}{c} \para  P_2\sub{c'}{d}}{\Phi,c':\bot}{\Delta \ominus \{\rho, \overline{\rho}\}} $$
and finally by typing rule \rulename{Restr} we can conclude
$$\judgement{\Gamma}{\Theta}{\restr{c'}{P_1\sub{c'}{c} \para  P_2\sub{c'}{d}}}{\Phi, c':\bot}{\Delta \ominus \{\rho, \overline{\rho}\}}$$ 

   \item [Case \rulename{r:I/O}]
We have that $P \equiv \inC{c}{\tilde{x}}.P_1 \para  \outC{c}{\tilde{e}}.P_2$ and  $$\judgebis{\env{\Gamma}{\Theta}}{\inC{c}{\tilde{x}}.P_1 \para  \outC{c}{\tilde{e}}.P_2}{ \type{\Phi', c:\bot}{\Delta}}$$ 
where $\Phi = \Phi', c:\bot$.

For Lemma \ref{lem:types}(\ref{types1}) there exists $\Phi_1, \Phi_2, \Delta_1$ and $\Delta_2$ such that $\Delta = \Delta_1 \uplus \Delta_2$, $$\Phi', c:\bot = \Phi_1, c:?(\tilde{\capab}).\rho \bowtie \Phi_2, c:!(\tilde{\capab}).\overline{\rho} $$ for some $\rho$ and 
\begin{enumerate}
 \item $\judgement{\Gamma}{\Theta}{\inC{c}{\tilde{x}}.P_1}{\Phi_1,c:?(\tilde{\capab}).\rho}{\Delta_1} $
 \item $\judgement{\Gamma}{\Theta}{\outC{c}{\tilde{e}}.P_2}{\Phi_2,c:!(\tilde{\capab}).\overline{\rho}}{\Delta_2} $
\end{enumerate}
Then from Lemma \ref{lem:types}(\ref{types2} and \ref{types3}) it follows
$\judgement{\Gamma,\tilde{x}:\tilde{\capab}}{\Theta}{P_1}{\Phi_1,c:\rho}{\Delta_1} \text{ and } \judgebis{\env{\Gamma}{\Theta}}{ P_2}{\Phi_2,c:\overline{\rho}} $
with $\Gamma \vdash \tilde{e}:\tilde{\capab}$.
Thus by Lemma \ref{lem:substitution}(2) and by using typing rule \rulename{Par}  we can conclude $$\env{\Gamma}{\Theta} \vdash P_1\sub{\tilde{e}}{\tilde{x}} \para  P_2: \type{\Phi}{\Delta} .$$

   \item [Case \rulename{r:Pass}]
We have that $P \equiv \catch{c}{d}.P_1 \para  \throw{c}{d}.P_2$ and  $$\judgebis{\env{\Gamma}{\Theta}}{\catch{c}{d}.P_1 \para  \throw{c}{d}.P_2}{ \type{\Phi', c:\bot, d:\sigma}{\Delta}}$$ 
where $\Phi = \Phi', c:\bot, d:\sigma$.

For Lemma \ref{lem:types}(\ref{types1}) there exists $\Phi_1, \Phi_2, \Delta_1$ and $\Delta_2$ such that $\Delta = \Delta_1 \uplus \Delta_2$, $$\Phi', c:\bot = \Phi_1, c:?(\sigma).\rho \bowtie \Phi_2, c:!(\sigma).\overline{\rho},d:\sigma $$ for some $\rho$ and 
\begin{enumerate}
 \item $\judgement{\Gamma}{\Theta}{\catch{c}{d}.P_1}{\Phi_1,c:?(\sigma).\rho}{\Delta_1} $
 \item $\judgement{\Gamma}{\Theta}{\throw{c}{d}.P_2}{\Phi_2,c:!(\sigma).\overline{\rho}, d:\sigma}{\Delta_2} $
\end{enumerate}
Then from Lemma \ref{lem:types}(\ref{typesdelin} and \ref{typesdelout}) it follows
$\judgement{\Gamma}{\Theta}{P_1}{\Phi_1,c:\rho, d:\sigma}{\Delta_1} \text{ and } \judgebis{\env{\Gamma}{\Theta}}{ P_2}{\Phi_2,c:\overline{\rho}} $.
Thus by using typing rule \rulename{Par}  we can conclude $$\env{\Gamma}{\Theta} \vdash P_1  \para  P_2: \type{\Phi}{\Delta} .$$


\item[Case \rulename{r:Rec}] We have that $P \equiv \rec{X:\type{\Phi}{\Delta}}{P'}$.
For Lemma \ref{lem:types}(\ref{types4}) we have  $\judgement{\Gamma}{\Theta, X:\type{\Phi}{\Delta}}{P}{\Phi}{\Delta} $.  
Now from Lemma \ref{lem:substitution}(3) we have $\judgement{\Gamma}{\Theta}{P\sub{\rec{X:\type{\Phi}{\Delta}}{P}}{X}]}{\Phi}{\Delta}$ thus concluding this case.



\item[Cases \rulename{r:IfTr} and \rulename{r:IfFa}] Follow from Lemma \ref{lem:types}(\ref{types5}).

\item[Case \rulename{r:Upd}] We have $P \equiv \component{l}{0}{\Delta}{P'} \para  \updated{l}{X}{\Delta}{\Delta'}{U}$ and $\judgebis{\env{\Gamma}{\Theta}}{\component{l}{0}{\Delta}{P'} \para  \updated{l}{X}{\Delta}{\Delta'}{U}}{ \type{\emptyset}{\Delta}}$
For Lemma \ref{lem:types}(\ref{types1}, \ref{types6} and \ref{types7}) we have that 
$\judgement{\Gamma}{\Theta}{P'}{\emptyset}{\Delta} $ and  $\judgebis{\env{\Gamma}{\Theta,\mathsf{X}:\type{\emptyset}{\Delta}}}{ U}{\type{\emptyset}{ \Delta'}}$. By Lemma \ref{lem:substitution} (4) we obtain $\judgement{\Gamma}{\Theta}{ U\sub{P'}{\mathsf{X}}}{\emptyset}{\Delta'}$. Thus concluding 
$$\judgement{\Gamma}{\Theta}{U\sub{P_1}{\mathsf{X}} \para  \nil}{\emptyset}{\Delta'} .$$




\item[Case \rulename{r:Close}] This case follows the same lines of  \rulename{r:Open} case and uses Lemma \ref{lem:types}(\ref{types9}).

\item[Case \rulename{r:Branch}] This case is similar to  previous \rulename{r:I/O} case where Lemma \ref{lem:types}(\ref{types12} and \ref{types13}) is used.




\item[Case \rulename{r:Str}] Follows by theorem \ref{th:congr}.

\item[Case \rulename{r:Res}] Follows by induction on the derivation tree and by using Lemma \ref{lem:types}(\ref{types10} and \ref{types11}).
\end{description}
\qed
\end{proof}

The three items in the statement of Theorem~\ref{th:subred} correspond to %the changes on type $\type{\Phi}{\Delta}$ that are due to 
the different possibilities for reduction.
Item~(1) is related to rules 
\rulename{r:I/O}, \rulename{r:Pass},
\rulename{r:Rec}, \rulename{r:IfTr}, \rulename{r:IfFa}, \rulename{r:Close}, \rulename{r:Res}, \rulename{r:Str}, and \rulename{r:Sel}. 
Item~(2) captures the case of a reduction via rule \rulename{r:Upd}: the exact shape of 
$\Delta'$ is obtained from $\Delta$ by considering the update process that has changed some located process 
with interface $\Delta_1$ into a process with interface $\Delta_2$. 
Item~(3) follows from \rulename{r:Open}.


\begin{remark}
With the tentative rules \rulename{t:IdeaCRes}, \rulename{t:IdeaPar}, \rulename{t:IdeaOpen}
subject reduction should hold in the following way. When using OPEN, rather than removing session types from $\ActS$, 
we bracket them. This is a way of keeping them ``invisible'' inside $\ActS$. Rule for composition now takes 
the usual union of $\ActS_1$, $\ActS_2$ (no merging with $\bowtie$). This way, the composition of two OPEN processes
should lead to a $\ActS$ with two bracketed (dual) types.  Now, we modify rule for restriction so as to bracket dual, unbracketed types.
Brackets thus represent hiding.
In this setting,  subject reduction should hold, up to the names for bracketed types. See the sketch for the case of open, in page~\pageref{th:subred}.
\end{remark}

The main consequence of 
Thm.~\ref{th:subred} is the \emph{absence of communication errors}
for well-typed processes. 
It also 
allows us to prove that every session that is established along the evolution of a process is \emph{consistent}.
We can indeed state:

\begin{corollary}[Con\-sist\-ency by Typing]\label{cor:cons}
Suppose %\\%$P$ be a well-typed process. 
$\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}} $
is a well-typed process.
Then every session $\ST_\qua \in \INT$ %that can be established along the evolution of $P$, we have that 
is consistent, in the sense of Def.~\ref{d:consist}.
\end{corollary}

%Theorem~\ref{th:subred} allows us to prove that every session that is established along the evolution of a process is consistent, i.e., sessions inside  adaptable processes cannot be disrupted by an update. 
This result follows from Thm.~\ref{th:subred} 
by observing that 
enabling update actions only for 
located processes without active sessions (cf. rule \rulename{r:Upd}), essentially 
rules out the possibility of 
updating a location containing 
a communicating process $P_{\langle c \rangle}$, as defined above.
Indeed, our type system ensures that the annotations enabling update actions 
are correctly assigned and maintained along reduction.







%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%




\input{exserver}

\input{interface}

\input{conclud}

\bibliographystyle{abbrv}
\bibliography{referen}

\appendix
\section{Proofs}
\input{appendix}
\input{derivation}




\end{document}